Termination Proof Script

Consider the TRS R consisting of the rewrite rule

There are 4 dependency pairs:

The approximated dependency graph contains one SCC: {2,4,5}.

Consider the SCC {2,4,5}. By taking the AF π with π(app) = π(APP) = 1 together with the lexicographic path order with precedence * ≻ +, the rules in {4,5} are weakly decreasing and the rules in {1,2} are strictly decreasing. There is one new SCC.
- Consider the SCC {4,5}. The constraints could not be solved.

Tyrolean Termination Tool (0.04 seconds) --- May 3, 2006